\begin{figure}[t]
	\centering
	\footnotesize
		\begin{IEEEeqnarray*}{rCl}
			t_1:&~& \text{1\_\textbf{Call~} X509\_get\_pubkey(\_);}\\
			&~& \text{2\_\textbf{Call~} X509\_REQ\_set\_pubkey(\_, \textbf{1\_X509\_get\_pubkey\_arg\_0}) };\\
			t_2:&~& \text{1\_\textbf{Call~} X509\_get\_pubkey(\_);} \\
			&~& \text{2\_\textbf{Assume}(\textbf{1\_X509\_get\_pubkey\_arg\_0 != NULL}) }; \\
			&~& \text{3\_\textbf{Call~} X509\_REQ\_set\_pubkey(\_, \textbf{1\_X509\_get\_pubkey\_arg\_0}) }; \\
			t_3:&~& \text{1\_\textbf{Call~} X509\_get\_pubkey(\_);} \\
			&~& \text{2\_\textbf{Call~} check\_suite\_b(\textbf{1\_X509\_get\_pubkey\_arg\_0}, \_, \_) ;}
		\end{IEEEeqnarray*}	
	\caption{图~\ref{fig:1-1-example}中抽象路径提取结果}
	\label{fig:3-3-path-example}
\end{figure}
%~& \text{2\_\textbf{Assume}(\textbf{1_X509_get_pubkey_arg_0 != NULL}) }; &